n:, f:(n), i:(n-1). sum(f((i, i+1)(x)) | x < n) = sum(f(x) | x < n)   

latex

Definitions	i  j < k, AB, P & Q, A, False, P  Q, sum(f(x) | x < k), {i..j}, x:A. B(x), t  T, , x(s), (i, j), SQType(T), {T}, Prop, x. t(x), Unit, P  Q, i=j, , b, b, if b t else f fi, P  Q
Lemmas	ifthenelse wf, assert wf, not wf, bnot wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, bool wf, sum functionality, sum split, sum wf, le wf, flip wf, nat wf, int seg wf